Inference at * 1 
Iof proof for Lemma assert of eq int:



1. x : 
2. y : 
3. (x = y)
  x = y 

latex

 by Unfolds ``eq_int`` 3 

latex

 1: 

 1: 3. if x=y  then tt  else ff
 1:   x = y
 .

Definitions

(i = j)